i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da),
upd:update-spec(ds;da).
Normal(ds)
 Normal(da)
 (kecl-kinds(A). (isrcv(k)  i = destination(lnk(k))  Id) & k  dom(da))
 update-spec-decl(upd;ds)
 msg-spec-loc-decl(snd;i;da)
 "ecl"  dom(ds)
 R-Feasible(ecl-machine at i with state ecl

 R-Feasible(A

 R-Feasible(state variables ds

 R-Feasible(actions da

 R-Feasible(sends snd

 R-Feasible(updates upd) 

latex

Definitions

x:AB(x), P & Q, R ||- es.P(es), x:AB(x), P  Q, t  T, "$x", Id, Type, x.A(x), x:A. B(x), x. t(x), a:A fp B(a), Top, IdDeq, x  dom(f), b, A, ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, R-Feasible(R), msg-spec-loc-decl(snd;i;da), update-spec-decl(upd;ds), Knd, KindDeq, Prop, lnk(k), destination(l), s = t, isrcv(k), ecl-kinds(x), xL. P(x), Normal(da), Normal(ds), update-spec(ds;da), msg-spec(ds;da), ecl(ds;da)

Lemmas

ecl-realizes, fpf wf, ecl wf, msg-spec wf, update-spec wf, normal-ds wf, normal-da wf, l all wf, ecl-kinds wf, isrcv wf, ldst wf, lnk wf, Kind-deq wf, Knd wf, update-spec-decl wf, msg-spec-loc-decl wf, not wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, Id wf